es:ES, L:(Id List).
fischer(L)
 (e, e':E.
 fEvent(e)
  fEvent(e')
  (rank(e) = rank(e')  (:  ))
  (loc(e) = loc(e')  Id)
  (e = e')) 

latex

Definitions	S  T, x. t(x), True, T, {T}, SQType(T), , , t  T, P  Q, x:A. B(x), P  Q, P & Q, P  Q, t.2, x(s), t.1, False, A, A  B, A c B, P  Q, Dec(P), fEvent(e), fischer(L)
Lemmas	es-le antisymmetry, es-le-not-locl, intpair-less-antireflexive, pi2 wf, nat sq, pi1 wf, le wf, f-rank-increases, event system wf, fischer wf, es-E wf, f-event wf, f-rank wf, es-loc wf, Id wf, decidable es-locl